/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.util.List;
import java.util.Map;
import java.util.Set;

import alloy.ast.FindCommand;
import alloy.ast.Formula;
import alloy.ast.Leaf;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.MultiplicityExpr;
import alloy.ast.Node;
import alloy.ast.VarCreator;
import alloy.ast.Variable;
import alloy.type.BasicType;
import alloy.type.RelationType;

/**
 * A read-only interface to various information about the translatable AST.
 * @see ASTInfoVisitor
 */
public interface ASTInfo {
    /** Return the root of the translatable AST */
    public Formula getFormula();

    /** Return the command we are analyzing */
    public FindCommand getCommand();
    
    /**
     * @return the parent {@link Node} of the given {@link Node}, or <code>null</code>
     *         if the node is root of the AST.
     */
    public Node getParent(Node node_);

    /** @return <code>true</code> iff anc_ is an ancestor of node_ */
    public boolean isAncestor(Node anc_, Node node_);
    
    /** @return the {@link VarCreator} that defined the quantified variable with this {@link LeafId}. */
    public VarCreator getVarCreator(LeafId leafId_);

    /** Test whether the given {@link LeafId} is for a quantified variable. */
    public boolean isQuantVar(LeafId leafId_);
    
    /**
     * @return all {@link BasicType}s used in the formula.
     */
    public Set /* of BasicType */ getBasicTypes();

    /**
     * Return the {@link BasicType} object representing the special Int basic type,
     * or null if Int is not used in the model.
     */
    public BasicType getIntType(); 

    /**
     * Return the {@link MultiplicityExpr multiplicity} of the quantified variable or relation
     * with the given {@link LeafId}.
     */
    public MultiplicityExpr getLeafMultiplicity(LeafId leafId_);

    /**
     * @return the {@link Variable} object (from the variable's declaration) with the given {@link LeafId}
     */
    public Variable getVariable(LeafId leafId_);

    /** @return the {@link RelationType} of leaves with the given {@link LeafId}. */
    public RelationType getLeafType(LeafId leafId_);

    /**
     * Test whether a given leaf is a skolem constant.
     */
    public boolean isSkolemConstant(LeafId leafId_);

    /** @return {@link Map} from {@link LeafId} of each relation to
	a {@link LeafExpr} for that relation. */
    public Map /* LeafId->LeafExpr */ getRelationReps();

    /**
     * @return {@link Set} of {@link LeafId}s of relations.
     * @see RelationAllocator
     */
    public Set /* of LeafId */ getRelations();

    /**
     * Return a representative {@link Leaf} with the given {@link LeafId}.
     */
    public Leaf getLeafRep(LeafId leafId_);

    /**
     * Return the {@link List} of {@link LeafId}s of quantified variables
     * declared at the given given {@link Node}, in order of declaration.
     * The list is empty unless the node is a {@link VarCreator}.
     */
    public List /* of LeafId */ getVarsDeclaredAt(Node node_);

    /**
     * Return an integer identifying the given node of the translatable
     * AST.  Each node of the translatable AST is deterministically assigned
     * an integer ID that depends only on the input model (i.e. will be the
     * same on different runs, different machines etc).
     */
    public int getNodeID(Node node_);
}

